FDL - Nuprl Definition : rel_equivalent

Nuprl Definition : rel_equivalent

R1

R2 ==

x, y:T. (R1(x,y))

(R2(x,y))

clarification:

rel_equivalent(T;R1;R2) ==

x:T, y:T. (R1(x,y))

(R2(x,y))

Definitions x:A. B(x), P Q, f(a)

FDL editor aliases rel_equivalent